I can merge this. One question, though. Do we want to squash the commits into one when we merge? Github now allows for this and it helps keeping the history cleaner, IMHO. Any @MohammadAlTurany, @pzhristov , @dberzano, @Barthelemy any opinions?

I prefer squashing. One PR == one feature.

If one wants to see the detailed commits and comments, she can always click on the PR (which is automatically referenced by GitHub in the squashed commit) and look at the history.

Moreover we get rid of "merge commits".

As a "disadvantage", whoever works on master and creates PRs from her master (instead of creating it from a separate branch) will not be able to simply pull from the upstream master once the PR is merged, but a git fetch && git reset --hard upstream/master with a subsequent git push -f myrepo will be required.

Hi,
Fine for me, we should squash the commits and avoid merge commits (merge --ff-only).
@dberzano: We do not allow PR to the master, user can only PR to the dev branch.
best,
Mohammad

@MohammadAlTurany Yes of course, but I was referring to the source branch not to the destination one. I realize my comment was not so clear. If a user has her branch called dev and makes a PR to the dev branch upstream, the moment she wants to sync with upstream a git reset is mandatory and git pull can't be done. This is not a big deal IMHO and I keep preferring squash merges.

Ok, since no one else complained I merged this.